/*
 * Atomic Predicates for Transformers
 * 
 * Copyright (c) 2015 UNIVERSITY OF TEXAS AUSTIN. All rights reserved. Developed
 * by: HONGKUN YANG and SIMON S. LAM http://www.cs.utexas.edu/users/lam/NRL/
 * 
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * with the Software without restriction, including without limitation the
 * rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
 * sell copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 * 
 * 1. Redistributions of source code must retain the above copyright notice,
 * this list of conditions and the following disclaimers.
 * 
 * 2. Redistributions in binary form must reproduce the above copyright notice,
 * this list of conditions and the following disclaimers in the documentation
 * and/or other materials provided with the distribution.
 * 
 * 3. Neither the name of the UNIVERSITY OF TEXAS AUSTIN nor the names of the
 * developers may be used to endorse or promote products derived from this
 * Software without specific prior written permission.
 * 
 * 4. Any report or paper describing results derived from using any part of this
 * Software must cite the following publication of the developers: Hongkun Yang
 * and Simon S. Lam, Scalable Verification of Networks With Packet Transformers
 * Using Atomic Predicates, IEEE/ACM Transactions on Networking, October 2017,
 * Volume 25, No. 5, pages 2900-2915 (first published as IEEE Early Access
 * Article, July 2017, Digital Object Identifier: 10.1109/TNET.2017.2720172).
 * 
 * 
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH
 * THE SOFTWARE.
 */
package transformer;

import java.util.*;

import common.PositionTuple;

public abstract class AbstractStateTransfer {

    protected PositionTuple destination;
    protected Net net;
    protected HashMap<PositionTuple, HashSet<AbstractState>> reachsets_out;
    protected HashMap<PositionTuple, HashSet<AbstractState>> reachsets_in;

    public void reset_reachsets()
    {
        reachsets_out = new HashMap<PositionTuple, HashSet<AbstractState>> ();
        reachsets_in = new HashMap<PositionTuple, HashSet<AbstractState>> ();
    }

    public void addtoreachsets_out(AbstractState sn)
    {
        addtoreachsets(sn, reachsets_out);
    }

    public void removefromreachsets_out(AbstractState sn)
    {
        removefromreachsets(sn, reachsets_out);
    }

    public void addtoreachsets_in(AbstractState sn)
    {
        addtoreachsets(sn, reachsets_in);
    }

    public void removefromreachsets_in(AbstractState sn)
    {
        removefromreachsets(sn, reachsets_in);
    }

    private void addtoreachsets(AbstractState sn, HashMap<PositionTuple, HashSet<AbstractState>> reachsets)
    {
        if(!reachsets.containsKey(sn.getPosition()))
        {
            HashSet<AbstractState> newset = new HashSet<AbstractState>();

            reachsets.put(sn.getPosition(), newset);
        }

        reachsets.get(sn.getPosition()).add(sn);
    }

    private void removefromreachsets
    (AbstractState sn, HashMap<PositionTuple, HashSet<AbstractState>> reachsets)
    {
        if(reachsets.containsKey(sn.getPosition()))
        {
            reachsets.get(sn.getPosition()).remove(sn);
        }
    }

    /**
     * @param pt1
     * @param pt2
     */
    public void add_link(PositionTuple pt1, PositionTuple pt2)
    {
        net.addTopology(pt1, pt2);
        
        add_link_(pt1, pt2);
        add_link_(pt2, pt1);
    }

    private void add_link_(PositionTuple pt1, PositionTuple pt2)
    {
        if(reachsets_out.containsKey(pt1))
        {
            HashSet<AbstractState> out_states = (HashSet<AbstractState>) reachsets_out.get(pt1).clone();
            for (AbstractState s : out_states)
            {
                if(s.can_be_extended())
                {
                    // if there is already a next state with position pt, no need to extend it
                    // this means that an already existing link is added
                    if(s.getNextState(pt2) == null)
                    {
                        //System.out.println("to extend");
                        Traverse_recur(s, pt2);
                    }
                }
            }
        }
    }
    
    /**
     * first remove device, then add back
     * used for updating tree caused by rule update
     * @param dname
     */
    public void device_update(String dname)
    {
        ArrayList<PositionTuple> links = net.get_all_links(dname);
        
        for(int i = 0; i < links.size(); i = i+2)
        {
            del_link(links.get(i), links.get(i+1));
        }
        
        for(int i = 0; i < links.size(); i = i+2)
        {
            add_link(links.get(i), links.get(i+1));
        }
    }
    
    public double[] device_update_times(String dname)
    {
        double [] update_times = new double[2];
        ArrayList<PositionTuple> links = net.get_all_links(dname);
        
        long t1 = System.nanoTime();
        for(int i = 0; i < links.size(); i = i+2)
        {
            del_link(links.get(i), links.get(i+1));
        }
        long t2 = System.nanoTime();
        
        update_times[0] = (t2 - t1)/1000000.0;
        
        t1 = System.nanoTime();
        for(int i = 0; i < links.size(); i = i+2)
        {
            add_link(links.get(i), links.get(i+1));
        }
        t2 = System.nanoTime();
        
        update_times[1] = (t2 - t1)/1000000.0;
        
        return update_times;
    }


    /**
     * @param pt1
     * @param pt2
     */
    public void del_link(PositionTuple pt1, PositionTuple pt2)
    {
        del_link_(pt1, pt2);
        del_link_(pt2, pt1);

        net.removeTopology(pt1, pt2);
    }

    private void del_link_(PositionTuple pt1, PositionTuple pt2)
    {
        if(reachsets_out.containsKey(pt1))
        {
            HashSet<AbstractState> out_states = reachsets_out.get(pt1);
            ArrayList<AbstractState> to_del = new ArrayList<AbstractState> ();
            for(AbstractState s : out_states)
            {
                AbstractState nxtS = s.getNextState(pt2);

                ArrayList<AbstractState> invalid_states = nxtS.get_all_descendants();
                
                to_del.addAll(invalid_states);

                /*
                for(AbstractState i_s : invalid_states)
                {
                    removefromreachsets_in(i_s);
                    removefromreachsets_out(i_s);
                }*/
                
                to_del.add(nxtS);
                //removefromreachsets_in(nxtS);

                s.delNextState(nxtS);
            }
            
            for(AbstractState s : to_del)
            {
                removefromreachsets_in(s);
                removefromreachsets_out(s);
            }
        }
    }


    public AbstractStateTransfer(Net net)
    {
        this.net = net;

    }


    public abstract AbstractState getNxtStateLink(AbstractState s, PositionTuple pt);
    public abstract AbstractState getNxtStateFwd(Object iter_obj, AbstractState s);
    public abstract Iterator getForwardingEntries(AbstractState s);

    /**
     * extend the tree starting from state s and position pt
     * @param s
     * @param pt
     */
    public void Traverse_recur(AbstractState s, PositionTuple pt)
    {

        PositionTuple curpt = s.getPosition();
        HashSet<PositionTuple> nxtpts = net.LinkTransfer(curpt);
        AbstractState nxts = null;
        if(nxtpts == null)
        {
            return;
        }else{

            for(PositionTuple nxtpt : nxtpts)
            {
                if(nxtpt.equals(pt))
                {
                    nxts = getNxtStateLink(s, nxtpt);
                    /**
                     *  int faps = s.getAPSet();
                        nxts = new State(nxtpt,faps, s.getAlreadyVisited(), s.getPtAlreadyVisited());
                     */

                    s.addNextState(nxts);
                    addtoreachsets_in(nxts);


                    //if(nxts.loopDetected())
                    if(nxts.ptLoopDetected())
                    {
                        continue;
                    }
                    if(destination != null)
                    {
                        if(nxts.destDetected(destination))
                        {
                            continue;
                        }
                    }

                    // next one is the switch forwarding
                    /**
                        Box nxtd = net.getBox(nxtpt.getDeviceName());
                        if(nxtd == null)
                        {
                              continue;
                        }
                        int fwdaps = nxts.getAPSet();
                        HashMap<String, Integer> fwdset =  nxtd.ForwardAction(nxtpt.getPortName(), fwdaps);
                     */
                    Iterator iter = getForwardingEntries(nxts);
                    if(iter == null)
                    {
                        continue;
                    }else
                    {
                        //Iterator iter = fwdset.entrySet().iterator();
                        //for(String portname : fwdset.keySet())
                        while(iter.hasNext())
                        {
                            AbstractState fwdeds = getNxtStateFwd(iter.next(), nxts);
                            /**
                                    Map.Entry<String, Integer> oneentry = (Entry<String, Integer>) iter.next();
                                    PositionTuple fwdedpt = new PositionTuple(nxtpt.getDeviceName(), oneentry.getKey());
                                    //State fwdeds = new State(fwdedpt, fwdset.get(portname), nxts.getAlreadyVisited());
                                    State fwdeds = new State(fwdedpt, oneentry.getValue(), nxts.getAlreadyVisited(), 
                                                nxts.getPtAlreadyVisited());
                             */
                            nxts.addNextState(fwdeds);
                            //if(!fwdeds.loopDetected() && !fwdeds.destDetected(destination))
                            Traverse_recur(fwdeds);
                        }
                    }
                }
            }

        }
    }

    public void Traverse_recur(AbstractState s)
    {
        addtoreachsets_out(s);

        PositionTuple curpt = s.getPosition();
        HashSet<PositionTuple> nxtpts = net.LinkTransfer(curpt);
        AbstractState nxts = null;
        if(nxtpts == null)
        {
            return;
        }else{

            for(PositionTuple nxtpt : nxtpts)
            {
                nxts = getNxtStateLink(s, nxtpt);
                /**
                 *  int faps = s.getAPSet();
                        nxts = new State(nxtpt,faps, s.getAlreadyVisited(), s.getPtAlreadyVisited());
                 */

                s.addNextState(nxts);
                addtoreachsets_in(nxts);


                //if(nxts.loopDetected())
                if(nxts.ptLoopDetected())
                {
                    continue;
                }
                if(destination != null)
                {
                    if(nxts.destDetected(destination))
                    {
                        continue;
                    }
                }

                // next one is the switch forwarding
                /**
                        Box nxtd = net.getBox(nxtpt.getDeviceName());
                        if(nxtd == null)
                        {
                              continue;
                        }
                        int fwdaps = nxts.getAPSet();
                        HashMap<String, Integer> fwdset =  nxtd.ForwardAction(nxtpt.getPortName(), fwdaps);
                 */
                Iterator iter = getForwardingEntries(nxts);
                if(iter == null)
                {
                    continue;
                }else
                {
                    //Iterator iter = fwdset.entrySet().iterator();
                    //for(String portname : fwdset.keySet())
                    while(iter.hasNext())
                    {
                        AbstractState fwdeds = getNxtStateFwd(iter.next(), nxts);
                        /**
                                    Map.Entry<String, Integer> oneentry = (Entry<String, Integer>) iter.next();
                                    PositionTuple fwdedpt = new PositionTuple(nxtpt.getDeviceName(), oneentry.getKey());
                                    //State fwdeds = new State(fwdedpt, fwdset.get(portname), nxts.getAlreadyVisited());
                                    State fwdeds = new State(fwdedpt, oneentry.getValue(), nxts.getAlreadyVisited(), 
                                                nxts.getPtAlreadyVisited());
                         */
                        nxts.addNextState(fwdeds);
                        //if(!fwdeds.loopDetected() && !fwdeds.destDetected(destination))
                        Traverse_recur(fwdeds);
                    }
                }
            }

        }
    }

}
